T, T':Type, L:T List, y:T', f:({x:T| (x  L) }T').
(y  mapl(f;L))  (a:T. (a  L) & y = f(a)) 

latex

Definitions	x:A. B(x), mapl(f;l), map(f;as), Y, t  T, P  Q, x:A. B(x), A & B, P & Q, P  Q, P  Q, Prop, P  Q, {T}, l[i], {i..j}, ||as||, i  j < k, hd(l), nth_tl(n;as), if b t else f fi, ij, b, i<j, true, false, (x  l)
Lemmas	l member wf, mapl wf, cons member, select member, length wf1, non neg length, le wf